($\lambda$$A$,$B$,$p$,$z$. 2of($p$)) $\in$ $A$:Type$\rightarrow$$B$:($A$$\rightarrow$Type)$\rightarrow$$p$:$a$:$A$$\times$$B$($a$)$\rightarrow\downarrow$True$\rightarrow$$B$(1of($p$))